A:Type, as:(A List). ((as = []))  (||as||  1 ) 

latex

ProofTree

Definitions	False, , t  T, P  Q, P  Q, P & Q, Y, ||as||, A, P  Q, x:A. B(x), A  B, i  j
Lemmas	length wf1, ge wf, not wf, non neg length, cons neq nil